YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { del(.(x, .(y, z))) -> f(=(x, y), x, y, z) , f(true(), x, y, z) -> del(.(y, z)) , f(false(), x, y, z) -> .(x, del(.(y, z))) , =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) , =(.(x, y), nil()) -> false() , =(nil(), .(y, z)) -> false() , =(nil(), nil()) -> true() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { f(true(), x, y, z) -> del(.(y, z)) , f(false(), x, y, z) -> .(x, del(.(y, z))) , =(nil(), nil()) -> true() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [del](x1) = [2 1] x1 + [2] [3 0] [2] [.](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [1 0] [0] [f](x1, x2, x3, x4) = [1 1] x1 + [1 0] x2 + [2 0] x3 + [3 0] x4 + [1] [0 0] [0 0] [3 0] [3 0] [2] [=](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] [true] = [3] [0] [false] = [2] [1] [nil] = [2] [0] [u] = [0] [0] [v] = [0] [0] [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] This order satisfies the following ordering constraints: [del(.(x, .(y, z)))] = [2 0] x + [3 0] y + [3 0] z + [2] [3 0] [3 0] [3 0] [2] >= [2 0] x + [3 0] y + [3 0] z + [2] [0 0] [3 0] [3 0] [2] = [f(=(x, y), x, y, z)] [f(true(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [4] [0 0] [3 0] [3 0] [2] > [2 0] y + [3 0] z + [2] [3 0] [3 0] [2] = [del(.(y, z))] [f(false(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [4] [0 0] [3 0] [3 0] [2] > [1 0] x + [2 0] y + [3 0] z + [2] [0 0] [2 0] [3 0] [2] = [.(x, del(.(y, z)))] [=(.(x, y), .(u(), v()))] = [1 0] x + [1 0] y + [0] [0 0] [0 0] [1] >= [1 0] x + [1 0] y + [0] [0 0] [0 0] [1] = [and(=(x, u()), =(y, v()))] [=(.(x, y), nil())] = [1 0] x + [1 0] y + [2] [0 0] [0 0] [1] >= [2] [1] = [false()] [=(nil(), .(y, z))] = [1 0] y + [1 0] z + [2] [0 0] [0 0] [1] >= [2] [1] = [false()] [=(nil(), nil())] = [4] [1] > [3] [0] = [true()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { del(.(x, .(y, z))) -> f(=(x, y), x, y, z) , =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) , =(.(x, y), nil()) -> false() , =(nil(), .(y, z)) -> false() } Weak Trs: { f(true(), x, y, z) -> del(.(y, z)) , f(false(), x, y, z) -> .(x, del(.(y, z))) , =(nil(), nil()) -> true() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { =(.(x, y), nil()) -> false() , =(nil(), .(y, z)) -> false() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [del](x1) = [2 1] x1 + [0] [3 0] [0] [.](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [1 0] [0] [f](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [3 0] x4 + [0] [0 0] [0 0] [3 0] [3 0] [0] [=](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [true] = [0] [0] [false] = [0] [0] [nil] = [2] [0] [u] = [0] [0] [v] = [0] [0] [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] This order satisfies the following ordering constraints: [del(.(x, .(y, z)))] = [2 0] x + [3 0] y + [3 0] z + [0] [3 0] [3 0] [3 0] [0] >= [2 0] x + [3 0] y + [3 0] z + [0] [0 0] [3 0] [3 0] [0] = [f(=(x, y), x, y, z)] [f(true(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [0] [0 0] [3 0] [3 0] [0] >= [2 0] y + [3 0] z + [0] [3 0] [3 0] [0] = [del(.(y, z))] [f(false(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [0] [0 0] [3 0] [3 0] [0] >= [1 0] x + [2 0] y + [3 0] z + [0] [0 0] [2 0] [3 0] [0] = [.(x, del(.(y, z)))] [=(.(x, y), .(u(), v()))] = [1 0] x + [1 0] y + [0] [0 0] [0 0] [0] >= [1 0] x + [1 0] y + [0] [0 0] [0 0] [0] = [and(=(x, u()), =(y, v()))] [=(.(x, y), nil())] = [1 0] x + [1 0] y + [2] [0 0] [0 0] [0] > [0] [0] = [false()] [=(nil(), .(y, z))] = [1 0] y + [1 0] z + [2] [0 0] [0 0] [0] > [0] [0] = [false()] [=(nil(), nil())] = [4] [0] > [0] [0] = [true()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { del(.(x, .(y, z))) -> f(=(x, y), x, y, z) , =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) } Weak Trs: { f(true(), x, y, z) -> del(.(y, z)) , f(false(), x, y, z) -> .(x, del(.(y, z))) , =(.(x, y), nil()) -> false() , =(nil(), .(y, z)) -> false() , =(nil(), nil()) -> true() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { del(.(x, .(y, z))) -> f(=(x, y), x, y, z) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [del](x1) = [2 1] x1 + [0] [2 1] [2] [.](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [1 0] [3] [f](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [3 0] x4 + [2] [1 2] [0 0] [2 0] [3 0] [1] [=](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [2] [true] = [2] [1] [false] = [1] [2] [nil] = [2] [0] [u] = [0] [0] [v] = [0] [0] [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [2] This order satisfies the following ordering constraints: [del(.(x, .(y, z)))] = [2 0] x + [3 0] y + [3 0] z + [3] [2 0] [3 0] [3 0] [5] > [2 0] x + [3 0] y + [3 0] z + [2] [1 0] [3 0] [3 0] [5] = [f(=(x, y), x, y, z)] [f(true(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [4] [0 0] [2 0] [3 0] [5] > [2 0] y + [3 0] z + [3] [2 0] [3 0] [5] = [del(.(y, z))] [f(false(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [3] [0 0] [2 0] [3 0] [6] >= [1 0] x + [2 0] y + [3 0] z + [3] [0 0] [2 0] [3 0] [6] = [.(x, del(.(y, z)))] [=(.(x, y), .(u(), v()))] = [1 0] x + [1 0] y + [0] [0 0] [0 0] [2] >= [1 0] x + [1 0] y + [0] [0 0] [0 0] [2] = [and(=(x, u()), =(y, v()))] [=(.(x, y), nil())] = [1 0] x + [1 0] y + [2] [0 0] [0 0] [2] > [1] [2] = [false()] [=(nil(), .(y, z))] = [1 0] y + [1 0] z + [2] [0 0] [0 0] [2] > [1] [2] = [false()] [=(nil(), nil())] = [4] [2] > [2] [1] = [true()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) } Weak Trs: { del(.(x, .(y, z))) -> f(=(x, y), x, y, z) , f(true(), x, y, z) -> del(.(y, z)) , f(false(), x, y, z) -> .(x, del(.(y, z))) , =(.(x, y), nil()) -> false() , =(nil(), .(y, z)) -> false() , =(nil(), nil()) -> true() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [del](x1) = [2 1] x1 + [0] [3 0] [0] [.](x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [1 0] [0] [f](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [3 0] x4 + [3] [0 1] [0 0] [3 0] [3 0] [3] [=](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [2] [true] = [0] [0] [false] = [0] [1] [nil] = [0] [0] [u] = [0] [0] [v] = [0] [0] [and](x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [2] This order satisfies the following ordering constraints: [del(.(x, .(y, z)))] = [2 0] x + [3 0] y + [3 0] z + [5] [3 0] [3 0] [3 0] [6] > [2 0] x + [3 0] y + [3 0] z + [3] [0 0] [3 0] [3 0] [5] = [f(=(x, y), x, y, z)] [f(true(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [3] [0 0] [3 0] [3 0] [3] > [2 0] y + [3 0] z + [2] [3 0] [3 0] [3] = [del(.(y, z))] [f(false(), x, y, z)] = [1 0] x + [2 0] y + [3 0] z + [3] [0 0] [3 0] [3 0] [4] >= [1 0] x + [2 0] y + [3 0] z + [3] [0 0] [2 0] [3 0] [2] = [.(x, del(.(y, z)))] [=(.(x, y), .(u(), v()))] = [1 0] x + [1 0] y + [2] [0 0] [0 0] [2] > [1 0] x + [1 0] y + [1] [0 0] [0 0] [2] = [and(=(x, u()), =(y, v()))] [=(.(x, y), nil())] = [1 0] x + [1 0] y + [1] [0 0] [0 0] [2] > [0] [1] = [false()] [=(nil(), .(y, z))] = [1 0] y + [1 0] z + [1] [0 0] [0 0] [2] > [0] [1] = [false()] [=(nil(), nil())] = [0] [2] >= [0] [0] = [true()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { del(.(x, .(y, z))) -> f(=(x, y), x, y, z) , f(true(), x, y, z) -> del(.(y, z)) , f(false(), x, y, z) -> .(x, del(.(y, z))) , =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) , =(.(x, y), nil()) -> false() , =(nil(), .(y, z)) -> false() , =(nil(), nil()) -> true() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))